Search for: All records

Memory-trace Obliviousness (MTO) is a noninterference property: programs that enjoy it have neither explicit nor implicit information leaks, even when the adversary can observe the program counter and the address trace of memory accesses. Probabilistic MTO relaxes MTO to accept probabilistic programs. In prior work, we developed λobliv, whose type system aims to enforce PMTO [2]. We showed that lambda-obliv could typecheck (recursive) Tree ORAM [6], a sophisticated algorithm that implements a probabilistically oblivious key-value store. We conjectured that λobliv ought to be able to typecheck more optimized oblivious data structures (ODSs)[8], but that its type system was as yet too weak.In this short paper we show we were wrong: ODSs cannot be implemented in lambda-obliv because they are not actually PMTO, due to the possibility of overflow, which occurs when a oram_write silently fails due to a local lack of space. This was surprising to us because Tree ORAM can also overflow but is still PMTO. The paper explains what is going on and sketches the task of adapting the PMTO property, and lambda-obliv's type system, to characterize ODS security. 

An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. This paper presents Lambda Obliv, a core language whose type system enforces obliviousness. Prior work on type-enforced oblivious computation has focused on deterministic programs. Lambda Obliv is new in its consideration of programs that implement probabilistic algorithms, such as those involved in cryptography. Lambda Obliv employs a substructural type system and a novel notion of probability region to ensure that information is not leaked via the observed distribution of visible events. Probability regions support reasoning about probabilistic correlation and independence between values, and our use of probability regions is motivated by a source of unsoundness that we discovered in the type system of ObliVM, a language for implementing state of the art oblivious algorithms. We prove that Lambda Obliv's type system enforces obliviousness and show that it is expressive enough to typecheck advanced tree-based oblivious RAMs.